\section{Metóda rezolvent pre výrokovú logiku}

\begin{definicia}[Rezolventa]
    Nech $C_1$ a $C_2$ sú ľubovoľné klauzuly, 
    $L_1$ je literál z $C_1$, $L_2$ je literál z $C_2$ a literály $L_1,L_2$
    sú navzájom kontrárne. Vynechajme $L_1$ z $C_1$ a $L_2$ z $C_2$,
    dostaneme tak klauzuly $C_1', C_2'$.
    Disjunkciu $C_1' \lor C_2'$ nazveme rezolventou klauzúl $C_1$ a $C_2$.
\end{definicia}

\begin{priklad}
    Majme $C_1 = P \lor R$ a $C_2 = \neg P \lor Q$. Uvažujme kontrárnu dvojicu
    $P,\neg P$. Potom $C_1' = R$, $C_2'=Q$. Rezolventa je $R \lor Q$.
\end{priklad}

\begin{priklad}
    Majme $C_1= \neg P \lor Q\lor R$, $C_2 = \neg Q \lor S$.
    Kontrárna dvojica je $\neg Q$, $Q$ a rezolventa $\neg P \lor R \lor S$.
\end{priklad}

\begin{priklad}
    Majme klauzuly $C_1: \neg P \lor Q$ a  $C_2: \neg P \lor R$.
    Tieto klauzuly nemajú rezolventu.
\end{priklad}

\begin{veta}
    Nech $C_1$ a $C_2$ sú klauzuly a nech $C$ je ich rezolventa.
    Potom $C$ je logickým dôsledkom klauzúl $C_1$ a $C_2$.
\end{veta}
\begin{dokaz}
    Nech $C_1 = L \lor C_1'$, $C_2 = \neg L \lor C_2'$ a 
    $C = C_1' \lor C_2'$.
    Máme ukázať, že z pravdivosti $C_1, C_2$ vyplýva pravdivosť $C$.

    Uvažujme interpretáciu $I$ takú, že $C_1$ a $C_2$ sú v nej pravdivé.
    Rozoberieme si 2 možnosti:
    \begin{itemize}
    \item $L$ nie je pravdivý literál v $I$.
        Potom musí platiť, že $C_1'$ je pravdivý v $I$. Tým pádom je ale aj
        $C$ pravdivé v $I$.

    \item $\neg L$ nie je pravdivý literál v $I$.
        Potom je evidentne klauzula $C_2'$ pravdivá v $I$. 
        A zo toho vyplýva, že aj $C$ je pravdivé v $I$.
    \end{itemize}
\end{dokaz}

\begin{poznamka}
    Nech $C_1$, $C_2$ sú jednotkové klauzuly. Ak $C_1,C_2$ majú
    rezolventu, potom musia tvoriť kontrárnu dvojicu $L, \neg L$
    a rezolventou je prázdna (nesplniteľná) klauzula $C \equiv \eps$.
\end{poznamka}

Našim cieľom bude zovšeobecniť predchádzajúcu poznámku do
nasledujúceho variantu: Nech $S$ je množina klauzúl. Potom $S$ je
nesplniteľná práve vtedy keď z nej vieme nejakým spôsobom pomocou
rezolvent získať prázdnu klauzulu.
Teraz si to formálne rozpíšeme.

\begin{definicia}[Rezolvenčné odvodenie]
    Nech $S$ je množina klauzúl.
    Rezolvenčným odvodením klauzuly $C$ z množiny klauzúl $S$
    nazývame konečnú postupnosť klauzúl $C_1, C_2, \ldots, C_n$ 
    (kde $C_n \equiv C$) takú,
    že pre každé $i \in \{1,2,\dots,n\}$ platí:
    $C_i$ je buď z $S$ alebo $C_i$ je rezolventa niektorých klauzúl
    $C_j, C_k$ pre $j, k < i$.

    Ak $C$ je prázdna klauzula, potom takémuto odvodeniu hovoríme 
    zamietnutie odvodenia alebo tiež dôkaz nesplniteľnosti $S$.
\end{definicia}

\begin{definicia}
    Majme množinu klauzúl $S$ a klauzulu $C$.
    Hovoríme, že $C$ môžeme získať z $S$,
    ak existuje (rezolvenčné) odvodenie $C_1, \dots, C_m$ z množiny $S$ také, že
    $C_m \equiv C$.
\end{definicia}

\begin{priklad}
    Uvažujme množinu klauzúl $S=\{\neg P \lor Q,\ \neg Q,\ P\}$.
    Uvažujme nasledujúce rezolvenčné odvodenie
    \begin{itemize} 
	\item[1:] $ \neg P \lor Q $  -- z $S$
	\item[2:] $ \neg Q $ -- z $S$
	\item[3:] $ \neg P $ -- pravidlo rezolventy na 1,2
	\item[4:] $ P $ -- z $S$.
        \item[5:] $\eps$ -- pravidlo rezolventy na 3,4
    \end{itemize}
    Dostali sme prázdnu klauzulu a teda množina klauzúl $S$ nie je
    splniteľná.
\end{priklad}

\begin{priklad}
    \label{prikl:rezolvencne_odvodenie}
    Nech $S=\{P \lor Q,\ \neg P \lor Q,\ 
            P \lor \neg Q,\ \neg P \lor \neg Q\}$.
    Opäť vieme dokázať nesplniteľnosť množiny klauzúl $S$:

    \begin{itemize}
	\item[1:] $P \lor Q$ -- z $S$
	\item[2:] $\neg P \lor Q$ -- z $S$
	\item[3:] $P \lor \neg Q$ -- z $S$
	\item[4:] $\neg P \lor \neg Q$ -- z $S$
	\item[5:] $Q$ -- rezolventa 1,2
	\item[6:] $\neg Q$ -- rezolventa 3,4
        \item[7:] $\eps$ -- rezolventa 5,6
    \end{itemize}

    K tomuto odvodeniu môžeme navyše nakresliť aj jeho strom (obr.
    \ref{fig:strom_odvodenia}).

    \begin{figure}[h]
	\centering\includegraphics{img/11/odvodenie.1.mps}
	\caption{Strom rezolvenčného odvodenia z príkladu 
            \ref{prikl:rezolvencne_odvodenie}}
        \label{fig:strom_odvodenia}
    \end{figure}
\end{priklad}

\begin{poznamka}
    Pravidlom rezolventy smerujeme k tomu, že sa snažíme získať
    prázdnu klauzulu. Dôležité je, že je to silné pravidlo,
    t.j., že ak je množina $S$ nie je splniteľná, vieme prázdnu
    klauzulu naozaj odvodiť iba pomocou tohoto pravidla. Na začiatok
    začneme ekvivalenciou pravidla rezolventy a pravidla modus ponens.
\end{poznamka}

\begin{lema}
    Pravidlo modus ponens je ekvivalentné s pravidlom rezolventy.
\end{lema}

\begin{dokaz}
    Najskôr si ukážeme, že pomocou MP vieme dokázať pravidlo rezolventy:
    Chceme ukázať $A \implies B, \neg A \implies C \provable \neg B
    \implies C$.
    Postupujme nasledovne:
    \begin{itemize}
        \item[1.] $\provable (A \implies B) \implies (\neg B \implies
                \neg A)$ -- tvrdenie z výrokovej logiky
        \item[2.] $A \implies B \provable A \implies B$
        \item[3.] $A \implies B \provable \neg B \implies \neg A$ --
                MP 1,2
        \item[4.] $\provable (\neg B \implies \neg A) \implies
            ((\neg A \implies C) \implies (\neg B \implies C))$ --
                jednoduchý sylogizmus.
        \item[5.] $A \implies B \provable
            (\neg A \implies C) \implies (\neg B \implies C)$ -- MP
            3,4
        \item[6.] $\neg A \implies C \provable \neg A \implies C$
        \item[7.] $A \implies B, \neg A \implies C \provable
            \neg B \implies C$ -- MP 5,6
    \end{itemize}
    Poznamenajme pritom, že obidve využité tvrdenia výrokovej logiky
    sa dajú dokázať z axióm iba pomocou pravidla modus ponens.

    Naopak, uvažujme, že chceme pravidlo MP simulovať pomocou pravidla
    rezolventy. Teda chceme ukázať $A, A\implies B \provable B$.
    Použijeme nasledujúci trik:
    \begin{itemize}
        \item[1.] $A \equiv A \lor \eps$
        \item[2.] $A \implies B \equiv \neg A \lor B$
        \item[3.] $A \lor \eps, \neg A \lor B \provable \eps \lor B$
            -- použime pravidlo rezolventy na ekvivalentné zápisy
            formúl $A, A\implies B$
        \item[4.] $B \equiv \eps \lor B$ a teda
        \item[5.] $A,A\implies B \provable B$.
    \end{itemize}
\end{dokaz}

